\begin{tabbing}
(\=(Unfold `p{-}compose` ( 0)$\cdot$) \+
\\[0ex]CollapseTHEN (RepUR ``can{-}apply do{-}apply`` ( 0)$\cdot$)$\cdot$) 
\\[0ex]
\\[0ex]CollapseTHEN ((Subst' (($n$+$m$) {-} 1) $\sim$ ($n$+($m$ {-} 1)) ( 0)$\cdot$) 
\\[0ex]CollapseTHEN (((Try ((Complete (
\-\\[0ex]A\=uto$\cdot$))$\cdot$))$\cdot$) \+
\\[0ex]CollapseTHEN ((Subst' ($f$\^{}$n$+($m$ {-} 1)($x$)) $\sim$ ($f$\^{}$n$(do{-}apply($f$\^{}$m$ {-} 1;$x$))) ( 0)$\cdot$)
\\[0ex]
\\[0ex]CollapseTHEN (((Try ((Fold `do{-}apply` 0) 
\\[0ex]CollapseTHEN (Trivial)$\cdot$))$\cdot$) 
\\[0ex]CollapseTHEN (
\-\\[0ex](if ((0) = 0) then BackThruSomeHyp else BHyp (0) )$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$
\end{tabbing}